package org.eclipse.iota.rules;

import static org.eclipse.iota.bounds.BoundType.LOWER;
import static org.eclipse.iota.bounds.BoundType.UPPER;

import org.eclipse.iota.bounds.BoundType;
import org.eclipse.iota.bounds.OldIotaBoundCalculator;
import org.eclipse.iota.bounds.IotaBoundUtil;
import org.eclipse.iota.model.Clause;
import org.eclipse.iota.model.Constant;
import org.eclipse.iota.model.Equation;
import org.eclipse.iota.model.EquationType;
import org.eclipse.iota.model.Expression;
import org.eclipse.iota.model.Reference;
import org.eclipse.iota.model.Variable;
import org.eclipse.iota.rewrite.AbstractIotaRule;
import org.eclipse.iota.util.IotaEqualityUtil;
import org.eclipse.iota.util.IotaReplaceUtil;

/**
 * @author Christian Krause
 * @generated NOT
 */
public class UpdateBounds extends AbstractIotaRule {

	public void visit(Variable variable) {
		// Update the bounds in all clauses.
		//for (Clause clause : getPredicate().getBody()) {
		//	updateBound(variable, clause, LOWER);
		//	updateBound(variable, clause, UPPER);
		//}
	}
	
	
	protected void updateBound(Variable variable, Clause clause, BoundType type) {
				
		// Compute the bound.
		Reference reference = new Reference(variable);
		Constant bound = OldIotaBoundCalculator.calculateBound(reference, clause, type);		
		if (bound==null) return;
		IotaBoundUtil.makeExclusive(bound, type);
		
		boolean updated = false;
			
		for (int i=0; i<clause.getConstraints().size(); i++) {
			
			// Must be an equation.
			if (clause.getConstraints().get(i) instanceof Equation) {
				
				Equation equation = (Equation) clause.getConstraints().get(i);
				Expression left = equation.getLeft();
				Expression right = equation.getRight();
					
				// Lower or upper bound?
				if (type==LOWER) {
					
					// a > 17 or 17 < a
					if ((equation.getType()==EquationType.GREATER && right instanceof Constant && 
							IotaEqualityUtil.equals(reference, left)) || 
						(equation.getType()==EquationType.LESS && left instanceof Constant && 
								IotaEqualityUtil.equals(reference, right))) {
						
						if (updated) {
							// Remove the constraint.
							clause.getConstraints().remove(i--);
						}
						else if (right instanceof Constant && bound.isGreaterThan((Constant) right)) {
							equation.setRight(bound.copy());
							equation.setInferred(true);
						}
						else if (left instanceof Constant && bound.isGreaterThan((Constant) left)) {
							equation.setLeft(bound.copy());
							equation.setInferred(true);
						}
						updated = true;
					}
						
				} else {
						
					// a < 17 or 17 > a
					if ((equation.getType()==EquationType.LESS && right instanceof Constant && IotaEqualityUtil.equals(reference, left)) || 
						(equation.getType()==EquationType.GREATER && left instanceof Constant && IotaEqualityUtil.equals(reference, right))) {
						
						if (updated) {
							// Remove the constraint.
							clause.getConstraints().remove(i--);
						}
						else if (right instanceof Constant && bound.isLessThan((Constant) right)) {
							equation.setRight(bound.copy());
							equation.setInferred(true);
						}
						else if (left instanceof Constant && bound.isLessThan((Constant) left)) {
							equation.setLeft(bound.copy());
							equation.setInferred(true);
						}
						updated = true;
					}
						
				}
			}
		}
		
		// Not updated yet?
		if (!updated) {
			Equation constraint = IotaBoundUtil.makeConstraint(reference, bound, type);
			constraint.setInferred(true);
			clause.getConstraints().add(constraint);
		}
		
	}
	
	
	/*
	private Constraint inferRelation(Variable v1, Variable v2, EquationType type, Monotonicity mono) {
		
		Equation equation = new Equation(new Reference(v1), new Reference(v2));
		equation.setType(null);
		
		switch (mono) {
		
		case STRICTLY_INCREASING:
			if (type==GREATER || type==EQUAL) equation.setType(GREATER);
			break;
			
		case INCREASING:
			if (type==GREATER) equation.setType(GREATER); else
			if (type==EQUAL) {
				equation.setType(GREATER);
				IotaOperationUtil.subtract(equation.getRight(), new Constant(1));
			}			
			break;
		
		case IDENTITY:
			if (type!=EQUAL) return new Boolean(false);
			break;

		case DECREASING:
			if (type==LESS) equation.setType(LESS); else
			if (type==EQUAL) {
				equation.setType(LESS);
				IotaOperationUtil.add(equation.getRight(), new Constant(1));
			}			
			break;

		case STRICTLY_DECREASING:
			if (type==LESS || type==EQUAL) equation.setType(LESS);
			break;

		}
		
		if (equation.getType()!=null) {
			return equation;
		}
		
		return null;
	}
	*/
	
}
